In this study, we demonstrated how automated verification can be useful in
verifying industrial transformations. First, we described the
GM-to-AUTOSAR transformation that we have developed for General
Motors~\cite{ECMFApaper}. We also discussed an automated transformation
verification prototype that works on the declarative, non-recursive subset of
ATL and its application to our transformation. %that can be used to implement
% non-trivial transformations.
The prototype was able to uncover two bugs in the transformation that violated
two multiplicities in the AUTOSAR metamodel. We further discussed the
performance of the verification prototype by showing the translation and
constraint solving times for all the constraints over different scopes. 
% The numbers showed that as the scope increases, the constraint solving time
% dominates the translation time. Thus, we showed by evidence the practicality of
% using automated verification in industry, and the strengths and limitations of
% the approach.
The numbers showed that both the Translation times and the Constraint Solving
times grow exponentially with the scope. Nonetheless, analysis of the
transformation in sufficiently large scopes (up to 12) was possible. We conclude
that the application of our verification approach to the case study was
successful and provides evidence for its practicality, even in industrial
contexts.


For future work, this study can be extended in several ways. First,
other industrial transformations should be incorporated in the case study
to have a better idea of the practicality of using automated verification on
such transformations. Our case study explored a transformation that manipulates
metamodels that are considered large on an industrial scale. The transformation,
although far from being trivial, does not fully manipulate the two metamodels.
We conducted a couple of experiments that show that the verification problem
scales almost linearly when more independent rules are added. However, we still
need to investigate the performance on larger and more complex transformations. 
\begin{changebar}As a result of our demonstration of the effectiveness of our approach in migrating a subset of the GM metamodel to its AUTOSAR equivalent, engineers at General Motors have expressed interest in extending the transformation to the full scope of the GM metamodel.\end{changebar}
Second, incremental SAT solvers can be used in the bounded search approach to
improve the performance and the execution time of the approach, as suggested in
Section \ref{subsec:Scalability}.
Third, pruning of the manipulated metamodels or the transformation model can be applied before
executing the bounded search, as suggested in Section
\ref{subsec:threatsToValidity}.